# note: this might be wrong, should I not subtract 1 from every of the numbers to make coordinates from them
def non_occupied_position(x, y):
 return ( (x == 2) and (y <= 5) ) or ( (y == 4) and (4 <= x <= 8) ) or ((x == 10) and (4 <= y <= 11)) or ((2 <= x <= 8) and (7 <= y <= 8))

allVars = []
output = ""

rows = range(0,11)
cols = range(0,11)

for x in cols:
 colterm = ""
 for y in rows:
  term = ""
  nonOc = non_occupied_position(x,y)
  var = "v_{}_{}".format(x,y)
  var2 = var
  allVars.append(var2)
  if nonOc:
   var = "not "+var
   term = var
  else:
   illegal_terms = set()
   for x1 in cols:
    for y1 in rows:
     if(not non_occupied_position(x1,y1) and not (x == x1 and y == y1)  and\
     ( ( (x == x1 or y == y1) ) or\
     ((x-x1)**2 + (y - y1)**2 <= 6) )):
      illegal_terms.add("v_{}_{}".format(x1,y1))
   consequent = ""
   for t in illegal_terms:
    consequent += t+" "
   consequent = "(not (or "+consequent+"))"
   term = "implies "+var+" "+consequent
  term = "("+term+")"
  output += term
  #output += "\n"
  colterm += var2+" "
 colterm = "(or "+colterm+")"
 output = "(and "+output+" "+colterm+")"
 #output += "\n"
output = "(and "+output+")"

allVarsTerm = ""
for t in allVars:
 allVarsTerm += t+" "
allVarsTerm = "("+allVarsTerm+")"

preambel = "(benchmark sat\n:logic SAT\n:variables "+allVarsTerm+"\n:formula "+output+"\n)"


print preambel
